diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 60da294..b71d68d 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -84,6 +84,17 @@ jobs: run: cabal run gatework -- --netlist fixtures/shared.net --duration 8 --output /tmp/shared.vcd --set d0=0,e0=0,d1=1,e1=0 --at 2 e0=1 --at 4 e1=1 --at 6 e0=0 - name: Compare the shared bus demo with the golden file run: diff fixtures/shared.golden.vcd /tmp/shared.vcd + - name: Run the library adder demo + run: cabal run gatework -- --netlist fixtures/libadder.net --library fixtures/adderlib.net --duration 0 --output /tmp/libadder.vcd --set a0=1,a1=1,a2=0,a3=0,b0=1,b1=0,b2=1,b3=0,cin=0 + - name: Compare the library adder demo with the golden file + run: diff fixtures/libadder.golden.vcd /tmp/libadder.vcd + - name: Confirm a missing library file stops the run + run: | + if cabal run gatework -- --netlist fixtures/libadder.net --library fixtures/missing.net --duration 0 --output /tmp/none.vcd 2>/tmp/none.log; then + echo "expected the missing library to fail" + exit 1 + fi + grep -q "cannot read library file: fixtures/missing.net" /tmp/none.log - name: Confirm a failed assertion stops the run run: | if cabal run gatework -- --netlist fixtures/assert.net --duration 6 --output /tmp/fail.vcd --set a=1,b=1 2>/tmp/fail.log; then diff --git a/CHANGELOG.md b/CHANGELOG.md index c9fab20..4af858f 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -5,6 +5,26 @@ All notable changes to Gatework appear in this file. The format follows the Keep a Changelog convention. This project uses semantic versioning. +## [0.9.0.0] - 2026-08-03 + +### Added + +- Define reusable modules in separate library files. +- Load module libraries with the --library command-line option. +- Repeat --library to load more than one module library. +- A library file may contain only module definitions. +- A library module can use modules from another library. +- Reject a module name that appears more than once across files. +- Reject a main netlist that shadows a library module. +- Reject top-level declarations inside a library file. +- Prefix library parse errors with the file path. +- Add a library adder demo fixture and a golden waveform. +- Add deterministic tests and a QuickCheck property for library loading. + +### Fixed + +- Load library files with an explicit read error check. + ## [0.8.0.0] - 2026-08-03 ### Added diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 9befa95..a170ebf 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -37,6 +37,8 @@ Put deterministic tests and QuickCheck properties in `test/Spec.hs`. Add a netlist fixture in `fixtures/`. The file name ends with `.net`. +A demo may load module definitions with the `--library` option. +Add the library file to `fixtures/` too. Add a golden file when you add a demo. The file name ends with `.golden.vcd`. diff --git a/README.md b/README.md index 6093f70..40134ca 100644 --- a/README.md +++ b/README.md @@ -5,6 +5,7 @@ It parses a plain-text netlist, runs the circuit, and writes a VCD waveform file GTKWave and other waveform viewers can open the output. The simulator uses four logic values: low, high, unknown, and floating. Multi-bit buses use bracketed widths and slices. +Reusable modules can live in separate library files. ## Value @@ -20,6 +21,9 @@ You can do these tasks: - Use NAND, NOR, and XNOR gates alongside the basic gates. - Define reusable modules and instantiate them many times. - Build a hierarchical adder from half-adder and full-adder modules. +- Store reusable modules in separate library files. +- Load a module library with the `--library` option. +- Build a hierarchical adder from a module library file. - Open the VCD output in GTKWave and inspect the waveforms. - Verify gate behavior with QuickCheck property tests. - Compare the counter waveform with a repository golden file. @@ -53,10 +57,15 @@ The project has four library modules. The data flow is: ```text +library text -> parser -> library module table netlist text -> parser -> module table -> flattened netlist -> event queue -> waveform recorder -> assertion check -> VCD ``` The parser validates names, gate arity, drivers, clocks, and references. +The parser loads module definitions from library files. +A library file holds only module definitions. +The parser merges the main and library modules into one table. +The parser rejects a module name that appears in more than one file. The parser expands each instance into the module gates. The parser expands each bus into single-bit signals before simulation. The flattened netlist uses dotted names for instance signals. @@ -268,6 +277,19 @@ The full-adder module contains two half-adder instances. The top level joins four full-adder instances in a carry chain. The adder produces binary 1000 for three plus five. +## Module library adder demo + +Run the same adder with its modules in a separate file. + +```powershell +cabal run gatework -- --netlist fixtures/libadder.net --library fixtures/adderlib.net --duration 0 --output libadder.vcd --set a0=1,a1=1,a2=0,a3=0,b0=1,b1=0,b2=1,b3=0,cin=0 +``` + +The file `fixtures/libadder.net` holds only the top level. +The file `fixtures/adderlib.net` defines the half-adder and full-adder modules. +The `--library` option loads the module definitions. +The library adder produces the same waveform as the hierarchical adder. + ## Hierarchical counter demo Run the hierarchical four-bit counter. @@ -495,6 +517,9 @@ The file `fixtures/gates.golden.vcd` holds the gate demo waveform. The file `fixtures/haddader.golden.vcd` holds the hierarchical adder waveform. Its identifiers include dotted instance names such as `f0.p`. +The file `fixtures/libadder.golden.vcd` holds the module library adder waveform. +Its content matches the hierarchical adder golden file. + The file `fixtures/hcounter.golden.vcd` holds the hierarchical counter waveform. Its identifiers include dotted instance names such as `counter.d0`. @@ -785,6 +810,32 @@ Modules may contain instances of other modules. A circular chain of instances is an error. An instance that names a missing module is an error. +### Module libraries + +Store reusable module definitions in a separate file. +A library file holds only module definitions. +It cannot hold inputs, outputs, wires, gates, or instances. + +```text +# halfadd.net +module halfadd (a,b) -> (sum,carry) + gate XOR xsum (a,b) -> sum + gate AND carry (a,b) -> carry +end +``` + +Load the library when you run the tool. + +```powershell +cabal run gatework -- --netlist top.net --library halfadd.net +``` + +Repeat `--library` for more libraries. +A library module can use modules from another library. +A module name cannot appear in more than one file. +The main netlist cannot reuse a module name from a library. +An error names the library file that caused it. + ## Verification The test suite has two parts. @@ -793,11 +844,13 @@ Deterministic tests also cover NAND, NOR, and XNOR truth tables, module flatteni Deterministic tests also cover undefined and floating values, tri-state buffers, and their golden output. Deterministic tests also cover bus declarations, bitwise gates, bit references, slices, bus registers, bus assertions, bus module ports, and error cases. Deterministic tests also cover multi-driver resolution, scheduled driver changes, flip-flop output exclusivity, the shared-bus fixture, and its golden output. +Deterministic tests also cover module library loading, cross-library module references, duplicate module names, and library file validation. QuickCheck properties cover gate algebra, full adder correctness, scheduled input sampling, reset sampling, register width, and assertion soundness. QuickCheck properties also compare the hierarchical adder and counter with their flat versions. QuickCheck properties also cover the four-state model and the tri-state buffer truth table. QuickCheck properties also compare a bus circuit with a bitwise reference model. QuickCheck properties also compare the shared bus with a per-time resolution model. +QuickCheck properties also compare a library adder with its flat version. QuickCheck runs one hundred random cases for each property. The gate properties cover the complete truth table. @@ -814,13 +867,15 @@ The bus XOR property compares a bus gate with per-bit evaluation. The bus register property compares each register bit with a reference value. The bus hierarchy property shows that a bus module matches its flat circuit. The shared-bus property compares each resolved wire value with a per-time model. +The library adder property compares a library netlist with the flat adder. ## Test status All tests pass on GHC 9.6.7 with Cabal 3.14 in the bundled container. The CI workflow runs the same checks on Ubuntu with GHC 9.6.6. -Golden tests compare the complete counter, register, reset, two-bit register, assertion, gate, hierarchical adder, hierarchical counter, adder, tri-state, undefined-state, bus, and shared-bus VCD text. +Golden tests compare the counter, register, reset, two-bit register, assertion, gate, hierarchical adder, library adder, hierarchical counter, adder, tri-state, undefined-state, bus, and shared-bus VCD text. CI runs every demo and compares its output with the golden file. +CI confirms that a missing library file stops the run. ## Limitations @@ -843,7 +898,11 @@ The event order decides the result. A wide flip-flop uses one shared reset signal. Assertions use the settled value at each time. An assertion time beyond the run duration is an error. -A file defines its modules and its top level in one place. +A netlist file can define modules inline or load them from library files. +A library file holds only module definitions. +A library file cannot hold top-level declarations. +The main netlist cannot shadow a library module. +Two library files cannot define the same module. Modules flatten before simulation, so the VCD stays flat. A bus expands into single-bit signals, so the VCD stays flat. A flip-flop bus output must have a `wire` or `output` declaration. @@ -857,6 +916,7 @@ The dotted instance names are part of the VCD signal names. ## Roadmap +Release 0.9.0.0 completed module libraries. Release 0.8.0.0 completed multi-driver wire resolution. Release 0.7.0.0 completed multi-bit buses, bit references, slices, and bus module ports. Release 0.6.0.0 completed undefined and floating logic values and tri-state buffers. @@ -867,10 +927,9 @@ Release 0.2.0.0 completed scheduled input transitions. Remaining work: -1. Add module definitions in separate files. -2. Add a waveform report command. -3. Add whole-bus input values on the command line. -4. Add multi-bit values in the VCD timeline. +1. Add a waveform report command. +2. Add whole-bus input values on the command line. +3. Add multi-bit values in the VCD timeline. ## License diff --git a/app/Main.hs b/app/Main.hs index 78a660e..f5d19a7 100644 --- a/app/Main.hs +++ b/app/Main.hs @@ -2,7 +2,7 @@ module Main (main) where import Data.List (intercalate) import Gatework.Logic (Logic, logicChar, parseLogic) -import Gatework.Netlist (netlistSignals, parseNetlistFile) +import Gatework.Netlist (netlistSignals, parseNetlistFileWithLibraries) import Gatework.Simulator ( AssertionFailure (..) , Simulation @@ -23,10 +23,11 @@ data Options = Options , optionOutput :: FilePath , optionInputs :: [(String, Logic)] , optionScheduled :: [(Time, String, Logic)] + , optionLibraries :: [FilePath] } defaultOptions :: Options -defaultOptions = Options Nothing 16 "gatework.vcd" [] [] +defaultOptions = Options Nothing 16 "gatework.vcd" [] [] [] main :: IO () main = do @@ -40,7 +41,7 @@ run :: Options -> IO () run options = case optionNetlist options of Nothing -> failWith "--netlist is required" Just path -> do - parsed <- parseNetlistFile path + parsed <- parseNetlistFileWithLibraries (optionLibraries options) path case parsed of Left message -> failWith message Right netlist -> @@ -86,6 +87,8 @@ parseOptions arguments = parseMore defaultOptions arguments duration <- maybe (Left "--duration requires an integer") Right (readMaybe value) parseMore options {optionDuration = duration} rest "--output" : path : rest -> parseMore options {optionOutput = path} rest + "--library" : path : rest -> + parseMore options {optionLibraries = optionLibraries options ++ [path]} rest "--set" : assignments : rest -> do values <- parseAssignments assignments parseMore options {optionInputs = optionInputs options ++ values} rest @@ -117,9 +120,11 @@ failWith message = do usage :: String usage = intercalate "\n" - [ "gatework --netlist FILE [--duration N] [--output FILE] [--set signal=0,signal=1,signal=x,signal=z] [--at TIME signal=0,signal=1,signal=x,signal=z]" + [ "gatework --netlist FILE [--library FILE] [--duration N] [--output FILE] [--set signal=0,signal=1,signal=x,signal=z] [--at TIME signal=0,signal=1,signal=x,signal=z]" , "" , "Simulate a netlist and write a VCD waveform." + , "Use --library to load reusable module definitions from another file." + , "Repeat --library to load more than one module file." , "Use --at to change input signals at a fixed time during the run." , "Use x for an unknown value and z for a floating value." , "Check assert declarations in the netlist against the waveform." diff --git a/fixtures/adder.golden.vcd b/fixtures/adder.golden.vcd index 50e0fee..659727e 100644 --- a/fixtures/adder.golden.vcd +++ b/fixtures/adder.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.8.0.0 + gatework 0.9.0.0 $end $timescale 1ns $end $scope module gatework $end diff --git a/fixtures/adderlib.net b/fixtures/adderlib.net new file mode 100644 index 0000000..4768f3f --- /dev/null +++ b/fixtures/adderlib.net @@ -0,0 +1,17 @@ +# Reusable adder module library. +# A library file holds only module definitions. +# Load this file with the --library option. + +module halfadd (a,b) -> (sum,carry) + gate XOR xsum (a,b) -> sum + gate AND carry (a,b) -> carry +end + +module fulladd (a,b,cin) -> (sum,cout) + wire p + wire g + wire h + instance halfadd u1 (a,b) -> (p,g) + instance halfadd u2 (p,cin) -> (sum,h) + gate OR cout (g,h) -> cout +end diff --git a/fixtures/assert.golden.vcd b/fixtures/assert.golden.vcd index 96e2a2a..adbf145 100644 --- a/fixtures/assert.golden.vcd +++ b/fixtures/assert.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.8.0.0 + gatework 0.9.0.0 $end $comment assert y = 1 at 0 diff --git a/fixtures/bus.golden.vcd b/fixtures/bus.golden.vcd index c164c3a..2a447eb 100644 --- a/fixtures/bus.golden.vcd +++ b/fixtures/bus.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.8.0.0 + gatework 0.9.0.0 $end $comment assert x[0] = 1 at 0 diff --git a/fixtures/counter.golden.vcd b/fixtures/counter.golden.vcd index 48c1f1a..8b2f596 100644 --- a/fixtures/counter.golden.vcd +++ b/fixtures/counter.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.8.0.0 + gatework 0.9.0.0 $end $timescale 1ns $end $scope module gatework $end diff --git a/fixtures/gates.golden.vcd b/fixtures/gates.golden.vcd index 38113ee..b48f092 100644 --- a/fixtures/gates.golden.vcd +++ b/fixtures/gates.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.8.0.0 + gatework 0.9.0.0 $end $comment assert nand_out = 1 at 0 diff --git a/fixtures/haddader.golden.vcd b/fixtures/haddader.golden.vcd index d31be49..11ebc19 100644 --- a/fixtures/haddader.golden.vcd +++ b/fixtures/haddader.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.8.0.0 + gatework 0.9.0.0 $end $timescale 1ns $end $scope module gatework $end diff --git a/fixtures/hcounter.golden.vcd b/fixtures/hcounter.golden.vcd index 9b803a8..2211b2f 100644 --- a/fixtures/hcounter.golden.vcd +++ b/fixtures/hcounter.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.8.0.0 + gatework 0.9.0.0 $end $timescale 1ns $end $scope module gatework $end diff --git a/fixtures/libadder.golden.vcd b/fixtures/libadder.golden.vcd new file mode 100644 index 0000000..11ebc19 --- /dev/null +++ b/fixtures/libadder.golden.vcd @@ -0,0 +1,82 @@ +$date + generated deterministically by gatework +$end +$version + gatework 0.9.0.0 +$end +$timescale 1ns $end +$scope module gatework $end +$var wire 1 ! a0 $end +$var wire 1 " a1 $end +$var wire 1 # a2 $end +$var wire 1 $ a3 $end +$var wire 1 % b0 $end +$var wire 1 & b1 $end +$var wire 1 ' b2 $end +$var wire 1 ( b3 $end +$var wire 1 ) cin $end +$var wire 1 * sum0 $end +$var wire 1 + sum1 $end +$var wire 1 , sum2 $end +$var wire 1 - sum3 $end +$var wire 1 . cout $end +$var wire 1 / c1 $end +$var wire 1 0 c2 $end +$var wire 1 1 c3 $end +$var wire 1 2 f0.p $end +$var wire 1 3 f0.g $end +$var wire 1 4 f0.h $end +$var wire 1 5 f1.p $end +$var wire 1 6 f1.g $end +$var wire 1 7 f1.h $end +$var wire 1 8 f2.p $end +$var wire 1 9 f2.g $end +$var wire 1 : f2.h $end +$var wire 1 ; f3.p $end +$var wire 1 < f3.g $end +$var wire 1 = f3.h $end +$upscope $end +$enddefinitions $end +#0 +1! +1" +0# +0$ +1% +0& +1' +0( +0) +0* +0+ +1+ +0+ +0, +1, +0, +0- +1- +0. +0/ +1/ +00 +10 +01 +11 +02 +03 +13 +04 +05 +15 +06 +07 +17 +08 +18 +09 +0: +1: +0; +0< +0= diff --git a/fixtures/libadder.net b/fixtures/libadder.net new file mode 100644 index 0000000..bc7ec9c --- /dev/null +++ b/fixtures/libadder.net @@ -0,0 +1,33 @@ +# Hierarchical ripple-carry adder from a module library. +# The half-adder and full-adder modules live in adderlib.net. +# Load them with the --library option. + +input a0 +input a1 +input a2 +input a3 +input b0 +input b1 +input b2 +input b3 +input cin + +output sum0 +output sum1 +output sum2 +output sum3 +output cout + +wire sum0 +wire sum1 +wire sum2 +wire sum3 +wire cout +wire c1 +wire c2 +wire c3 + +instance fulladd f0 (a0,b0,cin) -> (sum0,c1) +instance fulladd f1 (a1,b1,c1) -> (sum1,c2) +instance fulladd f2 (a2,b2,c2) -> (sum2,c3) +instance fulladd f3 (a3,b3,c3) -> (sum3,cout) diff --git a/fixtures/reg2.golden.vcd b/fixtures/reg2.golden.vcd index db9a0ed..a0a4dc1 100644 --- a/fixtures/reg2.golden.vcd +++ b/fixtures/reg2.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.8.0.0 + gatework 0.9.0.0 $end $timescale 1ns $end $scope module gatework $end diff --git a/fixtures/register.golden.vcd b/fixtures/register.golden.vcd index 969a8bc..975d612 100644 --- a/fixtures/register.golden.vcd +++ b/fixtures/register.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.8.0.0 + gatework 0.9.0.0 $end $timescale 1ns $end $scope module gatework $end diff --git a/fixtures/reset.golden.vcd b/fixtures/reset.golden.vcd index 7073472..e2bdfa9 100644 --- a/fixtures/reset.golden.vcd +++ b/fixtures/reset.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.8.0.0 + gatework 0.9.0.0 $end $timescale 1ns $end $scope module gatework $end diff --git a/fixtures/shared.golden.vcd b/fixtures/shared.golden.vcd index 808e7e8..fd3ba91 100644 --- a/fixtures/shared.golden.vcd +++ b/fixtures/shared.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.8.0.0 + gatework 0.9.0.0 $end $comment assert y = z at 0 diff --git a/fixtures/tristate.golden.vcd b/fixtures/tristate.golden.vcd index 115fb5f..c997a15 100644 --- a/fixtures/tristate.golden.vcd +++ b/fixtures/tristate.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.8.0.0 + gatework 0.9.0.0 $end $comment assert y = z at 0 diff --git a/fixtures/unknown.golden.vcd b/fixtures/unknown.golden.vcd index ace6fe7..7823fc1 100644 --- a/fixtures/unknown.golden.vcd +++ b/fixtures/unknown.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.8.0.0 + gatework 0.9.0.0 $end $comment assert q = x at 0 diff --git a/gatework.cabal b/gatework.cabal index 5edf6e5..9596c5d 100644 --- a/gatework.cabal +++ b/gatework.cabal @@ -1,6 +1,6 @@ cabal-version: 3.0 name: gatework -version: 0.8.0.0 +version: 0.9.0.0 synopsis: Event-driven digital logic simulation in Haskell description: Gatework parses typed netlists, runs combinational gates and D @@ -10,7 +10,8 @@ description: disabled. Several gates can drive one wire, and the scheduler resolves the driver values into one wire value. Multi-bit buses use bracketed widths and slices. Modules and instances build reusable - circuits. + circuits. A module library file stores reusable module definitions. + The command-line tool loads libraries with the --library option. GTKWave and other waveform viewers can open the output. homepage: https://github.com/DanielCuevas1208/gatework bug-reports: https://github.com/DanielCuevas1208/gatework/issues diff --git a/src/Gatework/Netlist.hs b/src/Gatework/Netlist.hs index a6881eb..4184530 100644 --- a/src/Gatework/Netlist.hs +++ b/src/Gatework/Netlist.hs @@ -10,8 +10,11 @@ module Gatework.Netlist , netlistSignals , parseNetlist , parseNetlistFile + , parseNetlistFileWithLibraries + , parseNetlistWithLibraries ) where +import Control.Exception (IOException, try) import Control.Monad (foldM, unless) import Data.Char (isAlphaNum, isSpace, toUpper) import Data.List (foldl', nub) @@ -130,19 +133,85 @@ emptyNetlist :: Netlist emptyNetlist = Netlist [] [] [] [] [] [] [] parseNetlistFile :: FilePath -> IO (Either String Netlist) -parseNetlistFile path = parseNetlist <$> readFile path +parseNetlistFile = parseNetlistFileWithLibraries [] + +parseNetlistFileWithLibraries :: [FilePath] -> FilePath -> IO (Either String Netlist) +parseNetlistFileWithLibraries libraryPaths mainPath = do + mainOutcome <- tryReadFile mainPath + case mainOutcome of + Left _ -> pure (Left ("cannot read netlist file: " ++ mainPath)) + Right mainSource -> do + libraries <- readLibraries libraryPaths + pure (do + sources <- libraries + parseNetlistWithLibraries sources mainSource) + where + readLibraries :: [FilePath] -> IO (Either String [(FilePath, String)]) + readLibraries [] = pure (Right []) + readLibraries (path : rest) = do + outcome <- tryReadFile path + case outcome of + Left _ -> pure (Left ("cannot read library file: " ++ path)) + Right content -> fmap (fmap ((path, content) :)) (readLibraries rest) parseNetlist :: String -> Either String Netlist -parseNetlist source = do +parseNetlist = parseNetlistWithLibraries [] + +parseNetlistWithLibraries :: [(FilePath, String)] -> String -> Either String Netlist +parseNetlistWithLibraries libraries source = do + (libraryModules, sources) <- loadLibraries libraries (rawModules, rawDeclarations) <- parseStatements (usefulLines source) - let signatureModules = signatureOnlyModules rawModules - modules <- mapM (resolveRawModule signatureModules) rawModules - validateModules modules + combinedModules <- foldM addMainModule libraryModules (Map.elems rawModules) + let signatureModules = signatureOnlyModules combinedModules + modules <- mapM (resolveModule sources signatureModules) combinedModules + validateModulesWithSources sources modules declarations <- resolveTopLevel signatureModules rawDeclarations netlist <- flattenParsed (ParsedNetlist modules declarations) _ <- validateNetlist netlist pure netlist +loadLibraries :: [(FilePath, String)] -> Either String (Map String RawModule, Map String FilePath) +loadLibraries = foldM addLibrary (Map.empty, Map.empty) + +addLibrary :: (Map String RawModule, Map String FilePath) -> (FilePath, String) + -> Either String (Map String RawModule, Map String FilePath) +addLibrary (modules, sources) (path, content) = do + let libraryResult = parseStatements (usefulLines content) + (libraryModules, libraryDeclarations) <- case libraryResult of + Left message -> Left (path ++ ": " ++ message) + Right parsed -> Right parsed + unless (null libraryDeclarations) $ + Left (path ++ ": library files may contain only module definitions") + foldM (insertLibraryModule path) (modules, sources) (Map.elems libraryModules) + +insertLibraryModule :: FilePath -> (Map String RawModule, Map String FilePath) -> RawModule + -> Either String (Map String RawModule, Map String FilePath) +insertLibraryModule path (modules, sources) moduleDef + | Map.member name modules = Left (path ++ ": duplicate module: " ++ name) + | otherwise = Right (Map.insert name moduleDef modules, Map.insert name path sources) + where + name = rawModuleName moduleDef + +addMainModule :: Map String RawModule -> RawModule -> Either String (Map String RawModule) +addMainModule modules moduleDef + | Map.member name modules = Left ("duplicate module: " ++ name) + | otherwise = Right (Map.insert name moduleDef modules) + where + name = rawModuleName moduleDef + +resolveModule :: Map String FilePath -> Map String Module -> RawModule -> Either String Module +resolveModule sources signatureModules moduleDef = + case resolveRawModule signatureModules moduleDef of + Left message -> Left (withSource (rawModuleName moduleDef) message) + Right resolved -> Right resolved + where + withSource name message = case Map.lookup name sources of + Just path -> path ++ ": " ++ message + Nothing -> message + +tryReadFile :: FilePath -> IO (Either IOException String) +tryReadFile path = try (readFile path) + usefulLines :: String -> [(Int, String)] usefulLines source = [ (lineNumber, cleaned) @@ -647,8 +716,16 @@ duplicates values = nub [value | value <- values, count value values > 1] where count value = length . filter (== value) -validateModules :: Map String Module -> Either String () -validateModules modules = mapM_ validateModule (Map.elems modules) +validateModulesWithSources :: Map String FilePath -> Map String Module -> Either String () +validateModulesWithSources sources modules = + mapM_ validateOne modules + where + validateOne moduleDef = case validateModule moduleDef of + Left message -> Left (withSource (moduleName moduleDef) message) + Right () -> Right () + withSource name message = case Map.lookup name sources of + Just path -> path ++ ": " ++ message + Nothing -> message validateModule :: Module -> Either String () validateModule moduleDef = do diff --git a/test/Spec.hs b/test/Spec.hs index 34e1049..f66655a 100644 --- a/test/Spec.hs +++ b/test/Spec.hs @@ -3,9 +3,17 @@ module Main (main) where import Control.Monad (forM) import Data.Bits (xor) import Data.Either (isLeft) -import Data.List (foldl', sortOn) +import Data.List (foldl', isPrefixOf, sortOn) import Gatework.Logic (GateType (..), Logic (..), evalGate, parseLogic) -import Gatework.Netlist (Assertion (..), Netlist (..), netlistAssertions, netlistSignals, parseNetlist) +import Gatework.Netlist + ( Assertion (..) + , Netlist (..) + , netlistAssertions + , netlistSignals + , parseNetlist + , parseNetlistFileWithLibraries + , parseNetlistWithLibraries + ) import Gatework.Simulator ( AssertionFailure (..) , Simulation @@ -130,6 +138,14 @@ main = do putStrLn ("shared fixture failed to parse: " ++ message) exitFailure Right netlist -> pure netlist + adderlibSource <- readFile "fixtures/adderlib.net" + libadderSource <- readFile "fixtures/libadder.net" + libadder <- case + parseNetlistWithLibraries [("fixtures/adderlib.net", adderlibSource)] libadderSource of + Left message -> do + putStrLn ("libadder fixture failed to parse: " ++ message) + exitFailure + Right netlist -> pure netlist deterministic <- sequence [ testParser , testParserAcceptsCommentsAndBlankLines @@ -230,6 +246,16 @@ main = do , testGoldenBusVCD , testSharedBusFixture , testGoldenSharedVCD + , testLibraryNetlistUsesLibraryModules + , testLibraryModulesReferenceEachOther + , testLibraryDuplicateModule + , testLibraryDuplicateAcrossFiles + , testLibraryRejectsTopLevelDeclarations + , testLibraryRejectsSyntaxError + , testLibraryUnknownModuleStillFails + , testLibraryFileEntryPoint + , testLibraryMissingFileFails + , testGoldenLibadderVCD ] properties <- forM [ ("AND is commutative", quickCheckResult propAndCommutative) @@ -273,6 +299,7 @@ main = do , ("bus register samples every bit", quickCheckResult propBusRegisterSampling) , ("bus module matches the flat circuit", quickCheckResult propBusModuleMatchesFlat) , ("shared bus follows the resolution model", quickCheckResult (propSharedBusResolution shared)) + , ("library adder matches the flat adder", quickCheckResult (propLibraryAdderMatchesFlat adder libadder)) ] $ \(label, action) -> do result <- action @@ -1563,6 +1590,164 @@ testGoldenSharedVCD = do pure (renderVCD simulation) check "shared bus VCD matches golden file" (actual == Right golden) +testLibraryNetlistUsesLibraryModules :: IO Bool +testLibraryNetlistUsesLibraryModules = + check "a netlist uses modules from a library file" $ case + parseNetlistWithLibraries + [ ( "adderlib.net" + , unlines + [ "module halfadd (a,b) -> (sum,carry)" + , " gate XOR xsum (a,b) -> sum" + , " gate AND carry (a,b) -> carry" + , "end" + ] + ) + ] + (unlines + [ "input a" + , "input b" + , "wire s" + , "wire c" + , "instance halfadd u1 (a,b) -> (s,c)" + ]) of + Right netlist -> + length (netlistGates netlist) == 2 + && netlistSignals netlist == ["a", "b", "s", "c"] + Left _ -> False + +testLibraryModulesReferenceEachOther :: IO Bool +testLibraryModulesReferenceEachOther = + check "library modules can use modules from another library" $ case + parseNetlistWithLibraries + [ ( "base.net" + , unlines + [ "module inv (a) -> (n)" + , " gate NOT g (a) -> n" + , "end" + ] + ) + , ( "top.net" + , unlines + [ "module twice (a) -> (n)" + , " wire m" + , " instance inv u1 (a) -> (m)" + , " instance inv u2 (m) -> (n)" + , "end" + ] + ) + ] + (unlines + [ "input a" + , "wire n" + , "instance twice u (a) -> (n)" + ]) of + Right netlist -> length (netlistGates netlist) == 2 + Left _ -> False + +testLibraryDuplicateModule :: IO Bool +testLibraryDuplicateModule = + check "a netlist cannot shadow a library module" $ case + parseNetlistWithLibraries + [ ( "adderlib.net" + , "module halfadd (a,b) -> (sum,carry)\n gate AND carry (a,b) -> carry\nend" + ) + ] + (unlines + [ "module halfadd (a,b) -> (sum,carry)" + , " gate XOR xsum (a,b) -> sum" + , "end" + , "input a" + , "input b" + , "wire s" + , "instance halfadd u1 (a,b) -> (s)" + ]) of + Right _ -> False + Left message -> message == "duplicate module: halfadd" + +testLibraryDuplicateAcrossFiles :: IO Bool +testLibraryDuplicateAcrossFiles = + check "two libraries cannot define the same module" $ case + parseNetlistWithLibraries + [ ( "first.net", "module m (a) -> (b)\n gate NOT g (a) -> b\nend" ) + , ( "second.net", "module m (a) -> (b)\n gate NOT g (a) -> b\nend" ) + ] + "input a\nwire b\ninstance m u (a) -> (b)\n" of + Right _ -> False + Left message -> message == "second.net: duplicate module: m" + +testLibraryRejectsTopLevelDeclarations :: IO Bool +testLibraryRejectsTopLevelDeclarations = + check "a library file rejects top-level declarations" $ case + parseNetlistWithLibraries + [ ( "badlib.net" + , unlines + [ "module m (a) -> (b)" + , " gate NOT g (a) -> b" + , "end" + , "input a" + ] + ) + ] + "input a\nwire b\ninstance m u (a) -> (b)\n" of + Right _ -> False + Left message -> message == "badlib.net: library files may contain only module definitions" + +testLibraryRejectsSyntaxError :: IO Bool +testLibraryRejectsSyntaxError = + check "a library syntax error names the file" $ case + parseNetlistWithLibraries + [ ( "broken.net", "module m (a) -> (b)\n gate NOT g (a) -> b\n bad line\nend\n" ) + ] + "input a\nwire b\ninstance m u (a) -> (b)\n" of + Right _ -> False + Left message -> "broken.net:" `isPrefixOf` message + +testLibraryUnknownModuleStillFails :: IO Bool +testLibraryUnknownModuleStillFails = + check "a missing module still fails with a library loaded" $ case + parseNetlistWithLibraries + [ ( "adderlib.net" + , "module halfadd (a,b) -> (sum,carry)\n gate AND carry (a,b) -> carry\nend" + ) + ] + "input a\ninput b\nwire s\ninstance missing u (a,b) -> (s)\n" of + Right _ -> False + Left message -> message == "instance references an unknown module: missing" + +testLibraryFileEntryPoint :: IO Bool +testLibraryFileEntryPoint = do + parsed <- parseNetlistFileWithLibraries ["fixtures/adderlib.net"] "fixtures/libadder.net" + case parsed of + Right netlist -> + check "the file entry point loads library modules" $ + length (netlistGates netlist) == 20 + Left _ -> check "the file entry point loads library modules" False + +testLibraryMissingFileFails :: IO Bool +testLibraryMissingFileFails = do + parsed <- parseNetlistFileWithLibraries ["fixtures/missing.net"] "fixtures/libadder.net" + case parsed of + Left message -> + check "a missing library file reports a clear error" $ + message == "cannot read library file: fixtures/missing.net" + Right _ -> check "a missing library file reports a clear error" False + +testGoldenLibadderVCD :: IO Bool +testGoldenLibadderVCD = do + librarySource <- readFile "fixtures/adderlib.net" + source <- readFile "fixtures/libadder.net" + golden <- readFile "fixtures/libadder.golden.vcd" + let actual = do + netlist <- + parseNetlistWithLibraries [("fixtures/adderlib.net", librarySource)] source + simulation <- simulateWithInputs netlist + [ ("a0", High), ("a1", High), ("a2", Low), ("a3", Low) + , ("b0", High), ("b1", Low), ("b2", High), ("b3", Low) + , ("cin", Low) + ] 0 + pure (renderVCD simulation) + check "library adder VCD matches golden file" (actual == Right golden) + evalTwoState :: GateType -> [Logic] -> Logic evalTwoState And inputs = if all (== High) inputs then High else Low evalTwoState Or inputs = if any (== High) inputs then High else Low @@ -1808,6 +1993,22 @@ propHierarchicalAdderMatchesFlat flat hierarchical = ) _ -> property False +propLibraryAdderMatchesFlat :: Netlist -> Netlist -> Property +propLibraryAdderMatchesFlat flat libraryBuilt = + forAll (choose (0, 15)) $ \a -> + forAll (choose (0, 15)) $ \b -> + forAll (elements [Low, High]) $ \carryIn -> + let expected = a + b + (if carryIn == High then 1 else 0) + in case ( simulateWithInputs flat (adderInputs a b carryIn) 0 + , simulateWithInputs libraryBuilt (adderInputs a b carryIn) 0 + ) of + (Right flatResult, Right libraryResult) -> + property + ( resultToInt flatResult == expected + && resultToInt libraryResult == expected + ) + _ -> property False + propHierarchicalCounterMatchesFlat :: Netlist -> Netlist -> Property propHierarchicalCounterMatchesFlat flat hierarchical = forAll (choose (0, 30)) $ \duration ->